package org.xteam.sled.semantic.exp;

import java.util.ArrayList;
import java.util.List;
import java.util.Set;

import org.xteam.sled.solver.SeparationResult;


public class TermList {
	
	public static class Term {

		private int factor;
		private Exp atom;

		public Term(int factor, Exp atom) {
			this.factor = factor;
			this.atom = atom;
		}
		
		public Exp toExpression(boolean negate) {
			int k = negate ? -factor : factor;
			if (k == 1)
				return atom;
			if (atom instanceof ExpConst)
				return new ExpConst(((ExpConst)atom).value()*k);
			return new ExpMul(k, atom);
		}
		
		public String toString() {
			return "[" + factor + "*" + atom + "]";
		}
		
	}

	private List<Term> terms = new ArrayList<Term>();

	public void add(int factor, Exp atom) {
		for (Term t : terms) {
			if (t.atom.equals(atom)) {
				t.factor += factor;
				if (t.factor == 0) {
					terms.remove(t);
				}
				return;
			}
		}
		terms.add(new Term(factor, atom));
	}
	
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		for (Term term : terms) {
			buffer.append(term.toString());
		}
		return buffer.toString();
	}

	public void normalize() {
		if (terms.size() > 0) {
			int k = Math.abs(terms.get(0).factor);
			for (int i = 1; i < terms.size(); ++i) {
				k = gcd(k, terms.get(i).factor);
			}
			if (k > 1) {
				for (int i = 0; i < terms.size(); ++i) {
					terms.get(i).factor /= k;
				}
			}
		}
	}
	
	/** find a candidate variable to extract from the equation.
	 * The variable is not an input, has a unity factor and
	 * does not appear in other terms.
	 * 
	 * @param inputs
	 * @return
	 */
	public String candidate(Set<String> inputs) {
		for (int i = 0; i < terms.size(); ++i) {
			Term t = terms.get(i);
			if (t.atom instanceof ExpVar) {
				String name = ((ExpVar)t.atom).name();
				if ((t.factor == 1 || t.factor == -1)
						&& ! inputs.contains(name)
						&& ! (freeInList(name, 0, i) || freeInList(name, i+1, terms.size()))) {
					return name;
				}
			}
		}
		return null;
	}
	
	public ExpCondition toConstraint() {
		Exp left = null;
		Exp right = null;
		for (Term t : terms) {
			if (t.factor > 0) {
				Exp f =  t.toExpression(false);
				left = left == null ? f : new ExpAdd(left, f);
			} else {
				Exp f =  t.toExpression(true);
				right = right == null ? f : new ExpAdd(right, f);
			}
		}
		if (left == null)
			left = new ExpConst(0);
		if (right == null)
			right = new ExpConst(0);
		return new ExpCondition(ExpCondition.EQ, left, right);
	}
	
	public Exp toSum() {
		Exp left = null;
		Exp right = null;
		for (Term t : terms) {
			if (t.factor > 0) {
				Exp f = t.toExpression(false);
				left = left == null ? f : new ExpAdd(left, f);
			} else {
				Exp f = t.toExpression(true);
				right = right == null ? f : new ExpAdd(right, f);
			}
		}
		if (left == null && right == null)
			return new ExpConst(0);
		if (right == null)
			return left;
		if (left == null)
			return right;
		return new ExpSub(left, right);
	}
	
	private boolean freeInList(String name, int from, int to) {
		IsFreeIn freeIn = new IsFreeIn(name);
		for (int i = from; i < to; ++i) {
			if (freeIn.get(terms.get(i).atom))
				return true;
		}
		return false;
	}
	
	public boolean hasUnknownVariable(Set<String> inputs) {
		IsUnknown isUnknown = new IsUnknown(inputs);
		for (Term t : terms) {
			if (isUnknown.get(t.atom))
				return true;
		}
		return false;
	}
	
	private static class IsFreeIn extends DefaultExpVisitor {
		
		private boolean hasName;
		private String name;

		public IsFreeIn(String name) {
			this.name = name;
		}

		public void visitVar(ExpVar expVar) {
			if (name.equals(expVar.name()))
				hasName = true;
		}

		public boolean get(Exp atom) {
			hasName = false;
			atom.visit(this);
			return hasName;
		}
	}
	
	private static class IsUnknown extends DefaultExpVisitor {
		
		private boolean isUnknown;
		private Set<String> names;

		public IsUnknown(Set<String> names) {
			this.names = names;
		}

		public void visitVar(ExpVar expVar) {
			if (! names.contains(expVar.name()))
				isUnknown = true;
		}

		public boolean get(Exp atom) {
			isUnknown = false;
			atom.visit(this);
			return isUnknown;
		}
	}

	/** Knuth vol 1, p 4 */
	private static int gcd(int m, int n) {
		if (n < 0) {
			n = -n;
		}
		if (m < n) {
			int t = m;
			m = n;
			n = t;
		}
		while (n != 0) {
			int r = m % n;
			m = n;
			n = r;
		}
		return m;
	}
	
	public SeparationResult findNonInputTerm(Set<String> inputs) {
		for (Term t : terms) {
			if (t.atom instanceof ExpVar) {
				String name = ((ExpVar)t.atom).name();
				if (! inputs.contains(name)) {
					//terms.remove(t);
					return new SeparationResult(name, t.factor, this);
				}
			}
		}
		return null;
	}

	public TermList eliminate(String var) {
		int factor = 1;
		for (Term t : terms) {
			if (t.atom instanceof ExpVar) {
				String name = ((ExpVar)t.atom).name();
				if (name.equals(var)) {
					terms.remove(t);
					factor = t.factor;
					break;
				}
			}
		}
		if (factor != 1 && factor != -1)
			throw new RuntimeException("bad factor");
		if (factor == 1) {
			for (Term t : terms) {
				t.factor = - t.factor;
			}
		}
		return this;
	}

}
